\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{ByteEval} (\coqdocvar{s}: \coqdocvar{State}) : \coqdocvar{ByteExp} \ensuremath{\rightarrow} \coqdocvar{option} \coqdocvar{Byte} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_lit} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{b}:\coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_num} \coqdocvar{b}) (\coqdocvar{Some} \coqdocvar{b})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_id} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqdocvar{Id})(\coqdocvar{b}:\coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{s} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{byte\_val} \coqdocvar{b}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_id} \coqdocvar{i}) (\coqdocvar{Some} \coqdocvar{b})\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_xor} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ByteExp})(\coqdocvar{b1} \coqdocvar{b2}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e1} (\coqdocvar{Some} \coqdocvar{b1}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e2} (\coqdocvar{Some} \coqdocvar{b2}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_xor} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{Some} (\coqdocvar{byte\_xor} \coqdocvar{b1} \coqdocvar{b2}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.50em}
\ensuremath{|} \coqdocvar{byte\_eval\_andbb} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e1} \coqdocvar{e2}: \coqdocvar{ByteExp})(\coqdocvar{b1} \coqdocvar{b2}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e1} (\coqdocvar{Some} \coqdocvar{b1}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e2} (\coqdocvar{Some} \coqdocvar{b2}) \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_andbb} \coqdocvar{e1} \coqdocvar{e2}) (\coqdocvar{Some} (\coqdocvar{byte\_and} \coqdocvar{b1} \coqdocvar{b2}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_shiftl} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e}: \coqdocvar{ByteExp})(\coqdocvar{x}: \coqdocvar{Integer})(\coqdocvar{n}: \coqdocvar{ArithExp})(\coqdocvar{b}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e} (\coqdocvar{Some} \coqdocvar{b}) \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{n} \coqdocvar{x} \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_shiftl} \coqdocvar{e} \coqdocvar{n}) (\coqdocvar{Some} (\coqdocvar{byte\_shl} \coqdocvar{b} \coqdocvar{x}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_shiftr} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{e}: \coqdocvar{ByteExp})(\coqdocvar{x}: \coqdocvar{Integer})(\coqdocvar{n}: \coqdocvar{ArithExp})(\coqdocvar{b}: \coqdocvar{Byte}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{ByteEval} \coqdocvar{s} \coqdocvar{e} (\coqdocvar{Some} \coqdocvar{b}) \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{n} \coqdocvar{x} \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_shiftr} \coqdocvar{e} \coqdocvar{n}) (\coqdocvar{Some} (\coqdocvar{byte\_shr} \coqdocvar{b} \coqdocvar{x}))\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{byte\_eval\_matrix} : \coqdockw{\ensuremath{\forall}} \coqdocvar{aexp1} \coqdocvar{aexp2} (\coqdocvar{m} \coqdocvar{n} \coqdocvar{i} \coqdocvar{j}: \coqdocvar{Integer})(\coqdocvar{mexp}: \coqdocvar{MatrixExp}) (\coqdocvar{matr}: \coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{MatrixEval} \coqdocvar{s} \coqdocvar{mexp} \coqdocvar{matr} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{aexp1} \coqdocvar{i} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{aexp2} \coqdocvar{j} \ensuremath{\rightarrow} \coqdocvar{ByteEval} \coqdocvar{s} (\coqdocvar{byte\_exp\_matrix} \coqdocvar{mexp} \coqdocvar{aexp1} \coqdocvar{aexp2}) (\coqdocvar{matrix\_get} \coqdocvar{i} \coqdocvar{j} \coqdocvar{matr})\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}